\chapter{FGJP Type Safety}
The proof is in line with the type safety proof of FGJ mentioned in \cite{FGJ}. Since we have added two new expressions(choice and parallel) and a new type i.e. void, some new cases are added and some cases are changed according to the new syntax. The cases that are added or changed are explicitly mentioned in different and italicfont.  

\section{Proof of Theorem 6.6.1}
Let us prove some lemma for developing the actual proof. \\
\subsection{Weakening}
{\it {\sffamily Suppose $\Delta, \ \overline{X} \prec: \overline{N} \ \vdash \ \overline{N} \ ok \ and \Delta \ \vdash \ U \ ok.$
\begin{itemize}
 \item If $\Delta \ \vdash \ \tau_1 \ \prec: \ \tau_2$ then $\Delta, \ \overline{X} \prec: \overline{N} \ \vdash \ \tau_1 \ \prec: \ \tau_2$
 \item If $\Delta \ \vdash \ \tau \ ok$ then $\Delta, \ \overline{X} \prec: \overline{N} \ \vdash \ \tau \ ok$
 \item {\it If $\Delta; \ \Gamma \ \vdash \ e\ : \ T$ then $\Delta, \ \overline{X} \prec: \overline{N} \ \vdash \ e \ :\ T$}
\end{itemize}
{\bf PROOF:} Each of them is  straightforward. $\Box$\\}}
\subsection{Inheritance transitivity}
If $\Delta \ \vdash \ E<\overline{V}> \ \prec: \ D<\overline{U}>$ and $D \ntrianglelefteq C \ and \ C\ntrianglelefteq D$ then $E \ntrianglelefteq C$ and $C \ntrianglelefteq E$ \\
{\bf PROOF:} E $\unlhd$ D since $\Delta \ \vdash E<\overline{V}> \ \prec: \ D<\overline{U}>$ is given. Suppose E $\unlhd$ C which means that either C $\unlhd$ D or D $\unlhd$ C. Contradiction. Hence E $\ntrianglelefteq$ C. Similar contradiction can be given for C $\ntrianglelefteq$ E.
\subsection{Downcast property}
Suppose dcast(C, D) and $\Delta \ \vdash \ C<\overline{T}> \ \prec:\ D<\overline{U}>$. If $\Delta \ \vdash \ C<\overline{T'}> \ \prec: \ D<\overline{U}> \ then \ T'\ = \ T$\\
{\bf PROOF: }Suppose D is direct superclass of C. Then by rule S-CLASS $D<\overline{U}>\ =\ [\overline{T}/\overline{X}]D<\overline{V}>$ for some $\overline{V}$ where CT(C) = class C$<\overline{X} \triangleleft \overline{N}>\ \triangleleft \ D<\overline{V}>$. Similarly, $D<\overline{U}>\ =\ [\overline{T'}/\overline{X}]D<\overline{V}>$. But the only free variables in $\overline{V}$ are $\overline{X}$ and replacing them with two other type variables is giving same result. This could be possible only if the two types are same. Hence T = T'. If D is not a direct superclass, the case will involve simple induction involving some intermediate type $E<\overline{V}>$ $\Box$
\subsection{Downcast inequality}
If dcast(C, E) and C $\unlhd$ D $\unlhd$ E with C $\neq$ D $\neq$ E then dcast(C, D) and dcast(D, E) \\
{\bf PROOF: } Easy $\Box$.
\subsection{Type substitution preserves subtyping}
If $\Delta_1, \ \overline{X} \ \prec: \ \overline{N}, \ \Delta_2 \ \vdash \ S\ \prec:\ T \ and \ \Delta_1 \ \vdash \ \overline{U} \ \prec: \ [\overline{U}/\overline{X}]\overline{N} \ with \ \Delta_1 \ \vdash \ \overline{U} \ ok $ and none of $\overline{X}$ appearing in $\Delta_1$ then $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]S \ \prec: \ [\overline{U}/\overline{X}]T$ \\
{\bf PROOF: }Cases S-REFL, S-VOIDSUB and S-VOIDSUP are trivial. \\
Case S-TRANS: simple induction.\\
Case S-VAR: S = X and T = ($\Delta_1, \ \overline{X} \ \prec: \ \overline{N}, \ \Delta_2$)(X) \\
If X $\in$ $dom(\Delta_1) \ \cup \ dom(\Delta_2$) then the claim is trivially true. If S = $X_i$ then $\Delta_1 \ \vdash \ U_i \ \prec: \ [\overline{U}/\overline{X}]N_i$. Hence proved. $\Box$
\subsection{Type substitution preserves well-formedness}
If $\Delta, \ \overline{X} \ \prec: \ \overline{N} \ \vdash \ \tau \ ok \ and \ \Delta_1 \ \vdash \overline{U}\  \prec: \ [\overline{U}/\overline{X}]\overline{N}\ with\ \Delta_1\ \vdash \ \overline{U} \ ok \ and\  $ $none\ of\ \overline{X} \ appearing\ in \ \Delta_1, \ then \ \Delta_1,\ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]\tau \ ok$\\
{\bf PROOF:} {\it {\sffamily WF-VOID and WF-OBJECT - Trivial}}\\
WF-VAR: $\tau$ = X and X $\in$ dom($\Delta_1, \ \overline{X} \ \prec: \ \overline{N}, \ \Delta_2$) \\
If X $\in$ $dom(\Delta_1) \ \cup \ dom(\Delta_2$) then $\Delta_1, \ \Delta_2 \ \vdash \ X \ ok$ else \\
X = X$_i$ implies $\Delta_1 \ \vdash \ U_i \ \prec: \ [\overline{U}/\overline{X}]\overline{N}$ and $\Delta_1 \ \vdash \ U_i \ ok$ which in turn implies that $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]\tau \ ok$\\
WF-CLASS: $\tau$ = T = C$<\overline{T}>$ \\
thus we have $\Delta_1, \ \overline{X}\prec: \overline{N},\ \Delta_2 \ \vdash \ \overline{T} \ ok $ \\
and $\Delta_1, \ \overline{X} \prec: \overline{N}, \ \Delta_2 \ \vdash \overline{T} \ \prec: \ [\overline{T}/\overline{Y}]\overline{P}$, class C$<\overline{Y}\triangleleft\overline{P}> \triangleleft \ N \ \{ ... \}$\\
$\Delta_1,\ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]\overline{T} \ \prec: \ [\overline{U}/\overline{X}][\overline{T}/\overline{Y}]\overline{P} $. Since $\overline{Y}\ \prec: \ \overline{P} \ \vdash \ \overline{P} \ ok$ by the rule GT-CLASS, $\overline{P}$ does not include any of $\overline{X}$ as a free variable. \\
Thus, $[\overline{U}/\overline{X}][\overline{T}/\overline{Y}]\overline{P} = [[\overline{U}/\overline{X}]\overline{T}/\overline{Y}]\overline{P}$ and hence $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ C<[\overline{T}/\overline{Y}]\overline{T}> \ ok$\\
{\sffamily WF-PROCESS: We know that:
\begin{center}
choose($e_1$, $e_2$) = $e_1.run()$ OR $e_e.run()$ \\
parallel($e_1$, $e_2$) = $e_1.run()$ AND $e_e.run()$ \\
\end{center}
Since $\Gamma; \ \Delta \ \vdash \ e_1 \ ok\ and \ e_2 \ ok$ \\
$\Gamma; \ \Delta \ \vdash \ e_1.run() \ ok \ and \ e_2.run() \ ok$ \\
And hence $\Gamma; \ \Delta \ \vdash \ choose(e_1, \ e_2) \ ok, \ parallel(e_1,\ e_2) \ ok \ \Box$ \\  }
\subsection{Bound property}
$\Delta_1, \ \overline{X} \ \prec: \ \overline{N}, \ \Delta_2 \ \vdash \ \tau \ ok\ and \ \Delta_1 \ \vdash \overline{U}\  \prec: \ [\overline{U}/\overline{X}]\overline{N}\ with\ \Delta_1\ \vdash \ \overline{U} \ ok \ and\  $ $none\ of\ \overline{X} \ appearing\ in \ \Delta_1, \ then \ \Delta_1, \ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ bound_{\Delta_1,[\overline{U}/\overline{X}]\Delta_2}([\overline{U}/\overline{X}]\tau)\ \prec:\ [\overline{U}/\overline{X}](bound_{\Delta_1,\overline{X}\prec:\overline{N}, \Delta_2}(\tau)) $\\
{\bf PROOF: }If $\tau$ is a non-variable type then it is trivially true. The case where $\tau$ is a type variable X and X $\in \ dom(\Delta_1)\cup dom(\Delta_2)$ is also straightforward. Finally if $\tau$ = $X_i$ bound$_{\Delta_1,[\overline{U}/\overline{X}]\Delta_2}([\overline{U}/\overline{X}]\tau) = U_i$
\\ and $[\overline{U}/\overline{X}]bound_{\Delta_1,\overline{X}\prec:\overline{N},\Delta_2}(\tau)=[\overline{U}/\overline{X}]N_i$ since $\Delta_1 \ \vdash \ \overline{U} \ \prec: \ [\overline{U}/\overline{X}]\overline{N}$ which implies $\Delta_1 \ \vdash \ U_i \ \prec: \ [\overline{U}/\overline{X}]N_i$. Hence proved. $\Box$\\
\subsection{Fields of superclass are retained}
If $\Delta \ \vdash \ S \ \prec: \ T$ and fields(bound$_{\Delta}$(T)) = $\overline{T} \ \overline{f}$ then fields(bound$_{\Delta}$(S)) = $\overline{S} \ \overline{g}$ and $S_i = T_i \ and  \ g_i = f_i$ for all i $\leq$ \#($\overline{f}$).\\
{\bf PROOF:} S-REFL is trivial. \\
S-VAR is straightforward since bound$_\Delta$(S) = bound$_\Delta$(T)\\
S-TRANS is simple induction \\
S-CLASS: S = C$<\overline{T}>$ and T = [$\overline{T}/\overline{X}$]N where the definition of C is $class \ C<\overline{X}\triangleleft\overline{N}>\ \triangleleft \ N \{ \overline{S} \ \overline{g}\}$\\ 
According to the rule F-CLASS $fields(C<\overline{T}>) \ = \ \overline{U} \ \overline{f}, \ [\overline{T}/\overline{X}]\overline{S} \ \overline{g}$ where $\overline{U} \ \overline{f} \ = \ fields([\overline{T}/\overline{X}]\overline{N}) \ 	\Box$. 
\subsection{Method overriding}
If $\Delta \ \vdash \ T \ ok, \ mtype(m, \ bound_{\Delta}(T)) = <\overline{Y}\triangleleft\overline{P}>\overline{U}\rightarrow \ \tau_o$ then for any S such that $\Delta \ \vdash \ S \ \prec; \ T$ and $\Delta \ \prec \ S \ ok$ we have $mtype(m, \ bound_{\Delta}(S)) = <\overline{Y}\triangleleft\overline{P}>\overline{U} \rightarrow \ \tau_o'$ and $\Delta, \ \overline{Y} \prec: \overline{P} \ \vdash \ \tau_o' \prec: \tau_o$\\
{\bf PROOF: } By simple induction on the derivation of $\Delta \ \vdash \ S \prec: T$\\
S-REFL, S-VOIDSUB and S-VOIDSUP are trivially true. \\
S-VAR: Trivial because bound$_\Delta$(S) = bound$_\Delta$(T)\\
S-TRANS: easy.\\
S-CLASS: S = C$<\overline{T}>$, T = [$\overline{T}/\overline{X}$]N where class C<$\overline{X}\triangleleft\overline{N}>\triangleleft N \ \{ ....\overline{M}\}$\\
If m $\notin \ \overline{M}$ then mtype(m, bound$_\Delta$(S)) = mtype(m, bound$_\Delta$(T)) else mtype(m, T) = $[\overline{T}/\overline{X}](<\overline{Y}\triangleleft\overline{P}>\overline{U}\rightarrow \ U_o'')$ = mtype(m, N) as well. Without loss of generality, we can say that $\overline{X}$ and $\overline{Y}$ are distinct and in particular that $[\overline{T}/\overline{X}]U_o''\ =\ U_o$. By GT-METHOD, we will have some method such that 
\begin{center}
 $<\overline{Y}\triangleleft\overline{P}> \ W_o' \ m(\overline{U'} \ \overline{x'}\{...\}) \ \in \ \overline{M}$
\end{center}
and 
\begin{center}
 $\overline{X}\prec:\overline{N}, \ \overline{Y} \ \prec: \ \overline{P'} \ \vdash \ W_o' \ \prec: \ U_o'' $
\end{center}
 By lemmas A.5 and A.1 we have, 
 \begin{center}
  $\Delta, \ \overline{Y}\prec: \overline{P} \ \vdash \ [\overline{T}/\overline{X}]W_o' \ \prec: \ U_o$.
 \end{center}
since mtype(m, bound$_\Delta$(S)) = mtype(m, S) = $[\overline{T}/\overline{X}](<\overline{Y}\triangleleft\overline{P}>\overline{U'}\rightarrow W_o')$ by MT-CLASS letting $U_o=[\overline{T}/\overline{X}]W_o'$, which finishes the case $\Box$.

\subsection{Type substitution preserves Typing}
If $\Delta_1, \ \overline{X} \ \prec: \ \overline{N}, \ \Delta_2 \ \vdash \ e \ : \ T \ and \ \Delta_1 \ \vdash \ \overline{U} \ \prec:[\overline{U}/\overline{X}]\overline{N}$ where $\Delta_1 \ \vdash \ \overline{U} \ ok$ and none of $\overline{X}$ appears in $\Delta_1$, then $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2; \ [\overline{U}/\overline{X}]\Gamma \ \vdash 
\ [\overline{U}/\overline{X}]e:S $ for some S such that $\Delta_1, [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ S \ \prec: \ [\overline{U}/\overline{X}]T$.\\
{\bf PROOF: }By induction on the derivation of $\Delta_1, \ \overline{X} \ \prec: \overline{N}, \ \Delta_2; \ \Gamma \ \vdash e\ :\ T$ with a case analysis on the last rule used. \\
GT-VAR: Trivial \\
GT-FIELD: 
% $e\ = \ e_o.f_i \ \ \Delta_1, \ \overline{X} \ \prec: \overline{N}, \ \Delta_2; \ \Gamma \ \vdash e_o\ :\ T_o$ \\
% fields(bound$_{\Delta_1, \ \overline{X} \ \prec: \overline{N}, \ \Delta_2}(T_o)$) = $\overline{T} \ \overline{f}$ \ \ T = $T_i$\\
% By induction hypothesis, $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2; [\overline{U}/\overline{X}]\Gamma \ \vdash \ [\overline{U}/\overline{X}]e_o:S_o \ and \ \Delta_1, \ [\overline{U}/\overline{X}]\Delta_2;  \ \vdash \ S_o \ \prec: \ [\overline{U}/\overline{X}]T_o$ for some $S_o$. By Lemma A.7,\\
% \begin{center}
%  $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2\ \vdash \ bound_{\Delta_1,[\overline{U}/\overline{X}]\Delta_2}([\overline{U}/\overline{X}]T_o) \ \prec: \ [\overline{U}/\overline{X}](bound_{\Delta_1, \ \overline{X} \ \prec: \overline{N}, \ \Delta_2}(T_o))$
% \end{center}
% Then, it is easy to show \\
% \begin{center}
%  $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2\ \vdash \ bound_{\Delta_1,[\overline{U}/\overline{X}]\Delta_2}([\overline{U}/\overline{X}]S_o) \ \prec: \ [\overline{U}/\overline{X}](bound_{\Delta_1, \ \overline{X} \ \prec: \overline{N}, \ \Delta_2}(T_o))$
% \end{center}
% By lemma A.8 fields$(bound_{\Delta_1,[\overline{U}/\overline{X}]\Delta_2}([\overline{U}/\overline{X}]S_o)) = \overline{S} \ \overline{g}$, and we have $f_i = g_i$ and $S_j = [\overline{U}/\overline{X}]T_j \ for \ j \leq \ \#(\overline{f})$.\\
% By rule GT-FIELD, $\Delta_1, [\overline{U}/\overline{X}]\Delta_2; [\overline{U}/\overline{X}]\Gamma \ \vdash \ [\overline{U}/\overline{X}]e_o.f_i:S_i$. Letting S = $S_i$ = $[\overline{U}/\overline{X}]T_i$, finishes the case.\\
% GT-INVK:
% \begin{center}
%  $e\ =\ e_o.m<\overline{V}>(\overline{e}) \ \ \ \Delta_1, \overline{X}\prec:\overline{N},\Delta_2; \ \Gamma \ \vdash \ e_o:T_o$\\
%  $mtype(m, \ bound_{\Delta_1, \overline{X}\ \prec: \ \overline{N}, \Delta_2}(T_o))\ = \ <\overline{Y}\triangleleft\overline{P}>\overline{W}\rightarrow \ W_o$\\
%  $\Delta_1, \overline{X}\prec: \overline{N}, \Delta_2 \ \vdash \ \overline{V} \ ok \ \Delta_1, \overline{X} \prec: \ \overline{N}],\Delta_2 \ \vdash \ \overline{V} \ \prec: \ [\overline{V}/\overline{Y}]\overline{P} $\\
%  $\Delta_1, \overline{X}\prec: \overline{N}, \Delta_2;\ \Gamma \ \vdash \ \overline{e}:\overline{S} \ \Delta_1, \overline{X} \prec: \ \overline{N}],\Delta_2 \ \vdash \ \overline{S} \ \prec: \ [\overline{V}/\overline{Y}]\overline{W} $\\
%   $T\ =\ [\overline{V}/\overline{Y}]W_o$
% \end{center}
% By the induction hypothesis,
% \begin{center}
%  $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2; [\overline{U}/\overline{X}]\Gamma \ \vdash \ [\overline{U}/\overline{X}]e_o:S_o$\\
%   $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2;  \ \vdash \ S_o \ \prec: \ [\overline{U}/\overline{X}]T_o$ 
% \end{center}
% and
% \begin{center}
%  $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2; [\overline{U}/\overline{X}]\Gamma \ \vdash \ [\overline{U}/\overline{X}]\overline{e}:\overline{S'}$\\
%   $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ \overline{S'} \ \prec: \ [\overline{U}/\overline{X}]\overline{S}$ 
% \end{center}
% By using lemma A.7, it is easy to show
% \begin{center}
%   $\Delta_1, \ [\overline{U}/\overline{X}]\Delta_2 \ \vdash \ bound_{\Delta_1,[\overline{U}/\overline{X}]\Delta_2}(S_o) \ \prec: \ [\overline{U}/\overline{X}](bound_{\Delta_1, \overline{X}\ \prec: \ \overline{N}, \Delta_2}(T_o))$
% \end{center}
% Then, by lemma A.9,
% \begin{center}
%   $mtype(m, \ bound_{\Delta_1, [\overline{U}/\overline{X}]\Delta_2}(S_o))\ = \ <\overline{Y}\triangleleft[\overline{U}/\overline{X}]\overline{P}>[\overline{U}/\overline{X}]\overline{W}\rightarrow \ W_o'$
% \end{center}
% By lemma A.6\\
% \begin{center}
%  $\Delta_1,[\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]\overline{V} \ ok$
% \end{center}
% Without loss of generality, we can assume that $\overline{X}$ and $\overline{Y}$ are distinct and that none of $\overline{Y}$ appear in $\overline{U}$; then $[\overline{U}/\overline{X}][\overline{V}/\overline{Y}] = [[\overline{U}/\overline{X}]\overline{V}/\overline{Y}][\overline{U}/\overline{X}]$. By lemma A.5 \\
% \begin{center}
%  $\Delta_1,[\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]\overline{V} \ \prec: [\overline{U}/\overline{X}][\overline{V}/\overline{Y}]\overline{P} \ \ (=[[\overline{U}/\overline{X}]\overline{V}/\overline{Y}][\overline{U}/\overline{X}]\overline{P})$\\
%   $\Delta_1,[\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [\overline{U}/\overline{X}]\overline{S} \ \prec: [\overline{U}/\overline{X}][\overline{V}/\overline{Y}]\overline{W} \ \ (=[[\overline{U}/\overline{X}]\overline{V}/\overline{Y}][\overline{U}/\overline{X}]\overline{W})$
% \end{center}
% By the rule S-TRANS,\\
% \begin{center}
%  $\Delta_1,[\overline{U}/\overline{X}]\Delta_2 \ \vdash \ [[\overline{U}/\overline{X}]\overline{V}/\overline{Y}][\overline{U}/\overline{X}]\overline{W}$
% \end{center}
% Finally, by the rule GT-INVK,\\
% \begin{center}
%  $\Delta_1,[\overline{U}/\overline{X}]\Delta_2, \ [\overline{U}/\overline{X}]\Gamma \ \vdash \ ([\overline{U}/\overline{X}]e_o).m<[\overline{U}/\overline{X}]\overline{V}>([\overline{U}/\overline{X}]\overline{d}):S$\\
% \end{center}
% where S = $[\overline{V}/\overline{Y}]W_o'$, finishing the case. \\
% GT-NEW, GT-CAST: Easy.\\
% GT-DCAST: 
% \begin{center}
% \begin{tabular}{ll}
%   e = (N)$e_o$ & $\Delta\ = \ \Delta_1, \overline{X} \ \prec: \ \overline{N}, \ \Delta_2$\\
%   $\Delta; \ \Gamma \ \vdash \ e_o:T_o$ & $\Delta \ \vdash \ N \ \prec: \ bound_{\Delta}(T_o)$\\
%   $N = C<\overline{T}>$ & $bound_{\Delta}(T_o) = E<\overline{V}> \ \ dcast(C, E)$
% \end{tabular}
% \end{center}
%  By the induction hypothesis, 
This case is exactly similar to the proof of FGJ. \\
GT-INVK, GT-NEw, GT-UCAST, GT-DCAST, GT-SCAST : Similar to FGJ.
\section{Term substitution preserves Typing}
If $\Delta; \ \Gamma, \ \overline{x}:\overline{T} \ \vdash \ e:T \ and \ \Delta;\Gamma \ \vdash \ \overline{d}:\overline{S} \ where\ \Delta \ \vdash \ \overline{S}\prec:\overline{T}, \ then \ \Delta;\Gamma \ \vdash \ [\overline{d}/\overline{x}]e:S$ for some S such that $\Delta \ \vdash S \prec:T$\\
{\bf PROOF: } The lemma can be proved by induction on the derivation of $\Delta;\Gamma, \ \overline{x}:\overline{T} \ \vdash \ e:T$ \\
GT-VAR: Similar to FGJ.\\
GT-FIELD: Similar to FGJ.\\
GT-INVK: 
\begin{center}
\begin{tabular}{ll}
 $e \ = \ e_o.m<\overline{V}>(\overline{e})$ & $\Delta; \Gamma, \ \overline{x}:\overline{T} \ \vdash \ e_o:T_o$\\
 mtype(m, bound$_\Delta(T_o)$) = $<\overline{Y}\unlhd>\overline{U}\rightarrow \ \tau$ & $\Delta \ \vdash \ \overline{V} \ ok$ \\
 $\Delta \ \vdash \ \overline{V} \ \prec: \ [\overline{V}/\overline{Y}]\overline{P}$ & $\Delta; \Gamma, \ \overline{x}:\overline{T} \ \vdash \ \overline{e}:\overline{S}$ \\
 $\Delta \ \vdash \ \overline{S} \ \prec: \ [\overline{V}/\overline{Y}]\overline{U}$ & $T = [\overline{V}/\overline{Y}]U$ 
\end{tabular}
\end{center}
By induction hypothesis, $\Delta; \Gamma \ \vdash \ [\overline{d}/\overline{x}]e_o:S_o$ for some $S_o$ such that $\Delta \ \vdash \ S_o \ \prec: \ T_o$ and $\Delta; \Gamma \ \vdash \ \ [\overline{d}/\overline{x}]\overline{e}:\overline{W}$ for some $\overline{w}$ such that $\Delta \ \vdash \ \overline{W}\ \prec: \ \overline{S}$. By lemma A.9, mtype(m, bound$_\Delta(S_o)$) = $<\overline{V}\unlhd>\overline{P}\rightarrow \ \tau'$ and $\Delta, \ \overline{Y} \ \prec: \ \overline{P} \ \vdash \ U' \ \prec: \ U$. By lemma A.5, $\Delta \ \vdash \ [\overline{V}/\overline{Y}]\tau' \ \prec: \ [\overline{V}/\overline{Y}]\tau$. By rule GT-METHOD, $\Delta; \Gamma \ \vdash \ [\overline{d}/\overline{x}](e_o.m<\overline{V}>(\overline{e})):[\overline{V}/\overline{Y}]\tau'$. This finishes the case.\\
CASE GT-NEW, GT-UCAST, GT-DCAST and GT-SCAST are similar to the proof of FGJ. Hence proved. $\Box$.\\

\section{Type substitution preserves method subtyping}
If $mtype(m, C<\overline{T}>)$ = $<\overline{Y}\unlhd>\overline{U}\rightarrow \ \tau$ and $mbody(m<\overline{V}>, \ C<\overline{T}>)\ = \ \overline{x}.e_o$ where $\Delta \ \vdash \ C<\overline{T}> \ ok \ and  \ \Delta \ \vdash \ \overline{V} \ \prec: \ [\overline{V}/\overline{Y}]\overline{P}$ then there exists some N and S such that $\Delta \ \vdash \ C<\overline{T}> \ \prec: N \ and \ \Delta \ \vdash \ N \ ok \ and \ \Delta \ \vdash \ S \ \prec: \ [\overline{V}/\overline{Y}]U \ and  \ \Delta\ \vdash \ S \ ok \ and \ \Delta; \overline{x}:[\overline{V}/\overline{Y}]\overline{U}, \ this:N \ \vdash \ e_o:S$\\
{\bf PROOF: } The lemma can be proved by induction on the derivation of $mbody(m<\overline{V}>, \ C<\overline{T}>)\ = \ \overline{x}.e_o$ using A.2, A.5 and A.10.\\
CASE MB-CLASS: class C$<\overline{Y}\triangleleft\overline{P}> \triangleleft \ N \ \{ ... \overline{M}\}$\\
$\overline{Y}\unlhd \overline{Q} \ \tau \ m(\overline{S} \ \overline{x})\{ \ return \ e; \ \} \ \in \ \overline{M}$\\
The case when $\tau$ = void is trivial since, [$\overline{V}/\overline{Y}$]void = void\\
The general case is similar to that for FGJ.\\
CASE GR-FIELD, GR-INVK, GR-CAST, GRC-FIELD, GRC-INVK-RECV, GRC-CAST, GRC-INV-ARG and GRC-NEW-ARG are similar to FGJ.\\
CASE GR-PROCESS:\\
{\sffamily If isProcess(e)=true then by F-PROCESS, e = new C$<\overline{T}>$ for some class C where $\Delta; \Gamma \ \vdash \ C \ \prec: \ Process$ and it has a method run implemented which returns a void. By rule GT-PROCESS-OP, the method call to run is valid and well-formed. And hence, $e_1$.run() $\cup$ $e_2$.run() reduces to the value choose($e_1,\ e_2$) and $e_1 \| \ e_2$ reduces to paralle($e_1, \ e_2$). $\Box$\\}	

% %\\\\\\\\\\\\\\\\\\\\\\
% \subsection{$If \ mtype(m,\  D)\  =\  \overline{C}\rightarrow\ \tau_o \  then \ mtype(m,\  C)\  =\  \overline{C}\rightarrow \ \tau_o\  for\ all\ C\ \prec:\ D$} 
% {\bf PROOF: } Straight forward induction on the derivation of C $\prec:$ D. According to the property of inheritance, whether m is defined in CT(C) or not, mtype(m, C) should be same as mtype(m, D) where C $\triangleleft$ E \{...\}.$\Box$\\
% 
% \subsection{Term-substitution preserves typing}$If \ \Gamma, \ \overline{x}:\overline{B}\ \vdash e\ : \ \tau,\ and\ \Gamma \ \vdash \ \overline{d}:\overline{A} \ where \overline{A}\ \prec: \ \overline{B},\ then \ \Gamma \ \vdash [\overline{d}/\overline{x}]e \ :\ \tau' \ for \ some\ \tau' \ \prec: \ \tau$\\
% {\bf PROOF:} 
